module tour/filesystem

// オブジェクト
abstract sig Object {}

// ディレクトリ
sig Directory extends Object {
	contents: set Object 
}

// ルートディレクトリ
one sig Root extends Directory {}

// ファイル
sig File extends Object {} 

// エイリアス(リンク)
sig Alias extends File {
	to: Object
}

// 制約 ルートディレクトリ以外のオブジェクトはいずれかのディレクトリに含まれる
fact ObjectBelongsSomewhere {
	all o : Object - Root | one d : Directory |
		o in d.contents
}

// 全てのディレクトリは自分の子のコンテンツとして出現してはならない
fact NoRecursiveDirs { 
	no d : Directory | d in d.^contents
}

// ルートディレクトリはディレクトリのコンテンツとして出現してはならない
fact RootHasNoSuperDir { 
	no d : Directory | Root in d.contents
}

// 全てのオブジェクトはルートディレクトリからたどれる
assert TrackableFromRoot {
	all o : Object | o in Root.*contents
}
//check TrackableFromRoot

pred show {}
run show for 10 but 5 Directory, 3 File
